perm filename UPDATE.NEW[1,JRA] blob
sn#024534 filedate 1973-02-07 generic text, type T, neo UTF8
00100
00200
00300 (DEFPROP UPDATE
00400 (LAMBDA(E)
00500 (PROG (USINGFL USING
00600 CHAN1
00700 ELOC
00800 CHAN
00900 AUTO
01000 DL1
01100 RF
01200 XYZ
01300 XYZ1
01400 CMD
01500 LOCFLG
01600 Z
01700 Z1
01800 Z2
01900 INCT
02000 Z3
02100 UEX
02200 Z1R
02300 Z2R
02400 N1
02500 R
02600 N
02700 NAME
02800 NAMELIST
02900 ZZ)
03000 (SETQ CHAN (OUTC NIL NIL))
03100 (SETQ AXNO (QUOTE INSERT))
03200 (SETQ FNNAM (QUOTE EDI))
03300 (SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
03400 (SETQ N1 (LAST NAMELIST))
03500 (SETQ INCT (INC NIL))
03600 U9 (SETQ ELOC E)
03700 (SETQ N 1)
03800 U3 (UP1A (CAR ELOC) N)
03900 U3A (TERPRI)
04000 U3AA (SETQ CMD (READ))
04100 (COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
04200 U3B (COND ((NOT (ATOM CMD)) (GO UPDATE1)))
04300 U3C (SETQ CMD (EXPLODE CMD))
04400 (COND ((EQ (LENGTH CMD) 1) (GO UER1))
04500 ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
04600 UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
04700 (GO U3A)
04800 UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
04900 (GO U3A)
05000 UDI1 (SETQ Z1 (UPGETL E NAMELIST))
05100 (COND ((NULL Z1) (GO U3A)))
05200 (CLAUSES Z1)
05300 (GO U3A)
05400 USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
05500 (SETQ Z NAMELIST)
05600 USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
05700 (SETQ Z (CDR Z))
05800 (COND (Z (GO USY2)))
05900 (GO U3A)
06000 UFL2 (SETQ Z (QUOTE U))
06100 (GO UFL4)
06200 UFL3 (SETQ Z (QUOTE D))
06300 (GO UFL4)
06400 UFL1 (SETQ Z (CAR (EXPLODE (READ))))
06500 UFL4 (SETQ Z2 405104)
06600 (COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
06700 UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
06800 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
06900 (UPDATESTATE (CDDR Z))
07000 (GO U3A)
07100 UDE1 (SETQ Z2 (UPGETL E NAMELIST))
07200 (COND ((NULL Z2) (GO U3A)))
07300 (EXPUNGE Z2)
07400 (GO U3A)
07500 UIN1 (SETQ NAME (READ))
07600 (SETQ Z2 (UPGETL E NAMELIST))
07700 (COND ((NULL Z2) (GO U3A)))
07800 UIN1A (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
07900 (NCONC Z1 Z2)
08000 (GO U3A)
08100 USU1 (SETQ Z1 (ERRSET (GETTERMS)))
08200 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
08300 ((NULL (CAR Z1)) (GO U3A)))
08400 (SETQ Z3 NIL)
08500 (SETQ Z1 (CAR Z1))
08600 USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
08700 (SETQ Z1 (CDR Z1))
08800 (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT))(SETQ Z2(SETUP Z3)) (GO UIN1A)))
08900 UUP1 (SETQ Z2 (UPGETNU))
09000 (COND ((NUMBERP Z2) (GO U8)) (T (GO U3A)))
09100 UDO1 (SETQ Z2 (UPGETNU))
09200 (COND ((NUMBERP Z2) (GO U7)) (T (GO U3A)))
09300 UAN1 (SETQ Z2 (UPGETL E NAMELIST))
09400 UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
09500 (SETQ Z2 (CDR Z2))
09600 (GO UAN2)
09700 UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
09800 (INC INCT)
09900 (OUTC CHAN NIL)
10000 (SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
10100 (SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
10200 (RETURN (MINIMIZE (APPEND Z1 Z)))
10300 USA1 (SETQ Z2 (UPGETL E NAMELIST))
10400 (COND (Z2 (NCONC E Z2)))
10500 (GO U3A)
10600 UPA1 (SETQ Z1 (UPGETL E NAMELIST))
10700 (SETQ Z2 (UPGETL E NAMELIST))
10800 (COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
10900 USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
11000 (COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
11100 (COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
11200 (SETQ Z3 Z1)
11300 (SETQ Z DDEPTH)
11400 (SETQ DDEPTH 22)
11500 USI2 (DEMOD (LIST (CAR Z3)) Z2)
11600 (SETQ Z3 (CDR Z3))
11700 (COND (Z3 (GO USI2)))
11800 (PRINT (QUOTE CLAUSES-ARE:))
11900 (CLAUSES Z1)
12000 (SETQ DDEPTH Z)
12100 (GO U3A)
12200 UAS1 (SETQ NAME (QUOTE ASSUMPTIONS))
12300 (GO UUS3)
12400 UCU1 (QUERY)
12500 (GO U3A)
12600 UDS1 (SETQ Z1 (READ))
12700 (COND ((NOT (ATOM Z1)) (GO UDS3)))
12800 UDS2 (COND
12900 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
13000 (GO UDS2)))
13100 UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
13200 (GO U3A)
13300 UEO1 (OUTC CHAN1 T)
13400 (GO U3A)
13500 UUS1 (SETQ NAME (QUOTE %USING))
13600 (SETQ USINGFL T)
13700 (SETQ USING NIL)
13800 UUS3 (SETQ LOCFLG T)
13900 UUS2 (SETQ Z2 (UPGETL E NAMELIST))
14000 (SETQ USINGFL NIL)
14100 (COND ((NULL Z2) (GO U3A)))
14200 USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
14300 (COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
14400 (T (RPLACA (CAR N1) NAME)
14500 (RPLACD (CAR N1) Z2)
14600 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
14700 (SETQ N1 (CDR N1))))
14800 (GO U3A)
14900 USE1 (SETQ NAME (READ))
15000 (SETQ LOCFLG NIL)
15100 (GO UUS2)
15200 UCL1 (SETQ Z (READ))
15300 UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
15400 ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
15500 (GO UCL2))
15600 (T (GO U3A)))
15700 UGO1 (SETQ Z1 (UPGETNU))
15800 (COND ((NOT (NUMBERP Z1)) (GO U3A)))
15900 (COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
16000 (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
16100 UTR1 (SETQ UEX NIL)
16200 (GO UEX2)
16300 UEX1 (SETQ UEX T)
16400 UEX2 (SETQ NAME (QUOTE LEMMA))
16500 (SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
16600 (COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
16700 (SETQ AUTO T)
16800 (SETQ Z2
16900 (ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
17000 (COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
17100 (T NIL))
17200 NIL))
17300 (SETQ AUTO NIL)
17400 (GO AT1A)
17500 UST1 (STOP)
17600 (GO U3A)
17700 UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
17800 (ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
17900 U8 (COND ((EQ Z2 0) (GO U9)))
18000 U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
18100 (SETQ Z2 (DIFFERENCE Z2 5))
18200 (SETQ ZZ 5)
18300 U84 (SETQ Z N)
18400 (SETQ Z3 (DIFFERENCE N ZZ))
18500 (COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
18600 (SETQ N Z3)
18700 (SETQ Z3 ELOC)
18800 (SETQ ELOC (DOWN N E))
18900 (SETQ ZZ NIL)
19000 (SETQ Z1 ELOC)
19100 U81 (COND ((EQ Z1 Z3) (GO U82)))
19200 (SETQ ZZ (CONS (CAR Z1) ZZ))
19300 (SETQ Z1 (CDR Z1))
19400 (GO U81)
19500 U82 (COND ((NULL ZZ) (GO U83)))
19600 (UP1A (CAR ZZ) (SUB1 Z))
19700 (SETQ ZZ (CDR ZZ))
19800 (SETQ Z (SUB1 Z))
19900 (GO U82)
20000 U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
20100 (SETQ Z2 (PLUS Z2 N))
20200 U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
20300 (SETQ ELOC (CDR ELOC))
20400 (SETQ N (ADD1 N))
20500 (UP1A (CAR ELOC) N)
20600 (COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
20700 UPR1 (TERPRI)
20800 (SETQ Z2 (UPGETL E NAMELIST))
20900 (COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
21000 (COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
21100 (SETQ AXNO (QUOTE THEOREM))
21200 (SETQ Z3 (NEGATE (CAR Z2)))
21300 (SETQ AXNO (QUOTE INSERT))
21400 (SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
21500 (COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
21600 (SETQ NAME (QUOTE LEMMA))
21700 (SETQ LOCFLG T)
21800 (GO USE2)
21900 UME1 (SETQ Z1 (UPGETL E NAMELIST))
22000 (SETQ Z2 (UPGETL E NAMELIST))
22100 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
22200 (BAKSUB Z1 Z2)
22300 (GO U3A)
22400 UHE1 (PRINT MESSAGE)
22500 (GO U3A)
22600 URE1 (SETQ Z1 (UPGETL E NAMELIST))
22700 (SETQ Z2 (UPGETL E NAMELIST))
22800 U%RE1
22900 (SETQ RF T)
23000 URE1A
23100 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
23200 (SETQ Z1R Z1)
23300 (SETQ Z2R Z2)
23400 (SETQ Z3 NIL)
23500 (COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
23600 (COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
23700 UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
23800 ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
23900 (COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
24000 (COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
24100 (SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
24200 UR3A (SETQ Z2R (CDR Z2R))
24300 (COND (Z2R (GO UR3)))
24400 (SETQ Z1R (CDR Z1R))
24500 (COND (Z1R (SETQ Z2R Z2) (GO UR3)))
24600 UR3B (COND ((NULL Z3)
24700 (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
24800 (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
24900 (RF (SETQ NAME (QUOTE RES)))
25000 (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
25100 (SETQ Z2 Z3)
25200 (SETQ LOCFLG T)
25300 (GO AT2A)
25400 UEV1 (PRINT (QUOTE EVAL-AWAITS))
25500 (SETQ Z2 (ERRSET (EVAL (READ)) T))
25600 (COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
25700 UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
25800 (GO UEV1)
25900 UPDATE1
26000 (SETQ Z (EXPLODE (CAR CMD)))
26100 (COND ((SETQ Z (ASSOC (READLIST (LIST (CAR Z) (CADR Z))) GOLIST1)) (GO (CDR Z))) (T (GO UER1)))
26200 AT1 (COND ((NULL (SETQ Z1 (GETNAME (CADR CMD) NAMELIST))) (GO U3A)))
26300 (SETQ NAME (CADR CMD))
26400 (SETQ XYZ Z1)
26500 (RPLACA (CDR CMD) (QUOTE XYZ))
26600 (RPLACA CMD (QUOTE ATTEMPTUNTIL))
26700 (SETQ Z2 (EVAL CMD))
26800 AT1A (UPDATESTATE STRAT)
26900 (COND
27000 ((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
27100 (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
27200 (PRINC NAME)
27300 (GO U3A))
27400 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
27500 (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
27600 (SETQ AUTO NIL)
27700 (GO AT1A))
27800 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
27900 (SETQ Z2 (CADR Z2))
28000 AT2A (SETQ N 1)
28100 AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
28200 (SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
28300 (PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
28400 (PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
28500 (PRIN1 NAME)
28600 (CLAUSES Z2)
28700 (GO USE2)
28800 S1 (COND ((NULL (SETQ XYZ (GETNAME (CADDDR CMD) NAMELIST))) (GO U3A)))
28900 (RPLACA (CDDDR CMD) (QUOTE XYZ))
29000 (RPLACA CMD (QUOTE SAVE))
29100 (EVAL CMD)
29200 (GO U3A)))
29300 EXPR)